$\forall$${\it es}$:ES\{i\}, $e$:E, $x$:Id. $e$ copies $x$ $\in$ Prop$_{\mbox{\scriptsize i'}}$